Nuprl Lemma : concat_iseg
11,40
postcript
pdf
T
:Type,
ll1
,
ll2
:(
T
List List).
ll1
ll2
concat(
ll1
)
concat(
ll2
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
l1
l2
,
x
:
A
.
B
(
x
)
,
t
T
,
,
Top
,
S
T
Lemmas
concat
wf
,
append
wf
,
concat
append
,
top
wf
origin
T:Type, ll1, ll2:(T List List). ll1 
ll2 
concat(ll1) concat(ll2) T:Type, ll1, ll2:(T List List). ll1 ll2 concat(ll1) concat(ll2) x:A. B(x) Q l2
x:A. B(x)
T
T